Nuprl Definition : unique_set
12,41
postcript
pdf
{!
x
:
T
|
P
(
x
)} == {
x
:
T
|
P
(
x
) & (
y
:
T
.
P
(
y
)
(
y
=
x
))}
latex
clarification:
{!
x
:
T
|
P
(
x
)} == {
x
:
T
|
P
(
x
) & (
y
:
T
.
P
(
y
)
(
y
=
x
T
))}
latex
Definitions
P
&
Q
,
x
:
A
.
B
(
x
)
,
P
Q
FDL editor aliases
unique_set
origin
y:T. P(y) 
(y = x))}
y:T. P(y) (y = x 
T))} y:T. P(y) (y = x))}
y:T. P(y) (y = x T))} x:A. B(x) Q